#!/usr/bin/env bash

# Usage:
#
# `./test` to build the AesopTest project and tests/*.lean
# `./test tests/<file>.lean ...` to build the specified files
#
# This script must be called from the directory it is located in.

GREEN="\e[0;92m"
RESET="\e[0m"

LEAN_OPTS="-D linter.unusedVariables=false"

# Build Aesop and AesopTest

lake build Aesop || exit 1
lake build AesopTest
exitcode="$?"

# Run golden tests in tests/

if [ -z "$1" ]; then
  files=(tests/*.lean)
else
  files="$@"
fi

function run_test {
  file="$1"
  expected="${file}.expected"
  produced="${file}.produced"
  lake env lean $LEAN_OPTS "$file" &> "$produced"
  if [ -f "$expected" ]; then
    diff "$expected" "$produced"
    return "$?"
  else
    echo "$expected not found, copying produced output"
    cp "$produced" "$expected"
    return 0
  fi
}

for file in ${files[@]}; do
  echo -e "$GREEN$file$RESET"
  run_test "$file"
  [ "$?" -eq 0 ] || exitcode=1
done

exit $exitcode
